(set-logic ALL)
(set-info :status unsat)
(declare-sort $$unsorted 0)
(declare-fun tptp.low () $$unsorted)
(declare-fun tptp.number_of_routines ($$unsorted $$unsorted $$unsorted) Bool)
(declare-fun tptp.high () $$unsorted)
(assert (forall ((A $$unsorted) (B $$unsorted)) (or (not (tptp.number_of_routines A B tptp.low)) (not (tptp.number_of_routines A B tptp.high)))))
(declare-fun tptp.organisation_at_time ($$unsorted $$unsorted) Bool)
(declare-fun tptp.efficient_producer ($$unsorted) Bool)
(declare-fun tptp.founding_time ($$unsorted $$unsorted) Bool)
(declare-fun tptp.has_elaborated_routines ($$unsorted $$unsorted) Bool)
(assert (forall ((A $$unsorted) (B $$unsorted)) (or (not (tptp.organisation_at_time A B)) (not (tptp.efficient_producer A)) (not (tptp.founding_time A B)) (tptp.has_elaborated_routines A B))))
(declare-fun tptp.first_mover ($$unsorted) Bool)
(assert (forall ((A $$unsorted) (B $$unsorted)) (or (not (tptp.organisation_at_time A B)) (not (tptp.first_mover A)) (not (tptp.founding_time A B)) (tptp.number_of_routines A B tptp.low))))
(declare-fun tptp.sk1 () $$unsorted)
(declare-fun tptp.sk2 () $$unsorted)
(assert (tptp.organisation_at_time tptp.sk1 tptp.sk2))
(assert (tptp.founding_time tptp.sk1 tptp.sk2))
(assert (tptp.number_of_routines tptp.sk1 tptp.sk2 tptp.high))
(assert (not (tptp.has_elaborated_routines tptp.sk1 tptp.sk2)))
(assert (forall ((A $$unsorted) (B $$unsorted)) (or (not (tptp.organisation_at_time A B)) (tptp.first_mover A) (tptp.efficient_producer A))))
(set-info :filename MGT041-2)
(check-sat)
